A:Realizer.  || A 

latex

Definitions	x:A. B(x), A || B, P  Q, t  T, Prop, Y, if b t else f fi, Rplus?(x1), P & Q, Rplus-left(x1), Rplus-right(x1), Rnone?(x1), True, false, true, AB, A, False, ij, , , Unit, P  Q, {T}, , S  T,
Lemmas	nat wf, R-size wf, nat plus inc, nat plus wf, es realizer wf, le wf, Rplus? wf, bool wf, eqtt to assert, R-size-decreases, Rplus-left wf, Rplus-right wf, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, nat properties, ge wf